A, C, B:Type, eqa:EqDecider(A), eqc, eqc':EqDecider(C), r:(AC), f:a:A fp B, a:A, z:B.
Inj(A; C; r)  rename(r;f)(r(a))?z = f(a)?z  B 

latex

Definitions	P  Q, x:A. B(x), A & B, {T}, False, Inj(A; B; f), EqDecider(T), f(x)?z, rename(r;f), Unit, P  Q, P & Q, x  dom(f), a:A fp B(a), Top, f(x), , Prop, b, A, t  T, b, x. t(x), x:A. B(x), P  Q
Lemmas	fpf-rename-ap2, assert wf, not wf, bnot wf, fpf-trivial-subtype-top, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, bool wf, top wf, fpf-rename wf, deq wf, fpf wf, inject wf, fpf-dom functionality2, fpf-rename-dom